Inference at * 2 
Iof proof for Lemma not over or:



1. A : 
2. B : 
3. (A  B)
  B 

latex

 by ((((((D 0) 
CollapseTHENM (D 3))) 
CollapseTHENM (Sel 2 (D 0)))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	t  T, P  Q, P  Q, A, False,
Lemmas	not wf, false wf